Inference at * 2 1 2 
Iof proof for Lemma before last:



1. T : Type
2. T List
3. u : T
4. v : T List
5. x:T. (x  v)  ((x = last(v)))  x before last(v)  v
6. x : T
7. x = u
8. (x = last([u / v]))
  [last(v)]  v 

latex

 by Assert (null(v)) 

latex

 1: .....assertion..... NILNIL

 1:   (null(v))
 2: 

 2: 9. (null(v))
 2:   [last(v)]  v
 .

Definitions

A, b, null(as)